type list =
| Nil  : list
| Cons : (int * list) -> list

inductive is_in : (int * list) ~> prop =
| forall (x, xs). is_in (x, Cons (x, xs))
| forall (x, y, xs). is_in (x, xs) => is_in (x, Cons (y, xs))

axiom: forall x. not (is_in (x, Nil))

lemma: forall (p, x, y, ys).
(forall x. is_in (x, Cons (y, ys)) => p (x)) =>
(forall x. is_in (x, ys) => p (x))

let rec list_exists (p, l) where (forall x. is_in (x, l) => pre (p) (x))
returns b
where ((b = true => exists x. is_in (x, l) and post (p) (x) (true))
  and  (b = false => forall x. is_in (x, l) => post (p) (x) (false))) =
match l with
  | Nil -> false
  | Cons (x, xs) -> if p (x) then true else list_exists (p, xs)
end
